Many phases of modern electronic design are performed with computer aided design (CAD) tools or electronic design automation (EDA) systems. An EDA system typically receives the high level behavior descriptions of the IC device and translates this high-level design language into netlists of various levels of abstraction using a computer synthesis process. A netlist describes, for example, interconnections of nodes and components on the chip and includes information of circuit primitives such as transistors and diodes, their sizes and interconnections.
After a designer has created an initial set of designs, the circuit designer and/or verification engineers may then test and optimize the design using a set of EDA testing and analysis tools. For example, at the logical level, simulation and formal verification may be used to test the IC design. At the physical implementation level, testing and optimization steps include extraction, verification, and compaction.
To perform simulation or formal verification, the simulation/verification tool must be able to access a model of the system being simulated/verified. A finite state machine (FSM) of the design can be used to create models or automata that is then simulated or formally verified. Circuit simulation uses the mathematical models to replicate the behavior of the circuit design given a set of test stimulus. Formal verification is the act of proving or disproving the correctness of the intended operation of the design, with respect to certain formal specifications or properties of the design.
The issue addressed by the present disclosure is that the process of performing these verification techniques have become more complicated in recent years due to the introduction of low-power designs. With the rapid growth of the wireless and portable electronic markets, there is a constant demand for new technological advancements, which has resulted in more and more functionality being incorporated into battery-operated products, increasing challenges for power management of such devices. Power concerns in server farm and base station are also becoming higher priority. Such challenges include, for example, minimization of leakage power dissipation, designing efficient packaging and cooling systems for power-hungry ICs, or verification of functionality or power shut-off sequences early in the design. These challenges are expected to become even more difficult with the continuous shrinking of process nodes using today's CMOS technology.
To address these low-power challenges, file formats such as UPF (“Unified Power Format”) and CPF (“Common Power Format”) have been developed that capture power-related design intent information, power-related power constraints, and/or power-related technology information for a circuit design. These files may be accessed and used by EDA tools throughout the EDA implementation flow to design and verify the integrated circuit.
For verification purposes, the information in these files are applied to potentially change the design behavior of components, which in some cases may actually introduce new components into the design during the verification process. For example, consider a module in the design where it is known that under certain conditions, the module will be either powered on or powered off. During either the power-off or power-on states, the verification system needs to understand the impacts of these states upon the operation of the design.
To explain, consider the combinational component (gate 130) and sequential component (134) illustrated in FIG. 1A. For the purposes of formal verification, when power is off to these components, then the outputs of these components may need to be modeled as a free net value.
To model the combinational gate 130 for this purpose in some cases, a transformation can be performed to add a multiplexer 132, where the input of the mux 132 is switched between the normal output of the gate or a free net value (“X”), and the selection of which input line is used for the mux is dependent upon whether the power is on or off (e.g., power off selects the free net and power on selects the original gate output). It is noted that this approach is merely one example of a transformation that may be performed, and one skilled in the art would understand that other types of transformations are also applicable to address this situation.
For the sequential component 134, the transformation for formal verification may create a new version 134′ of component 134 to make the register power-aware, e.g., where the synchronous register is converted into an asynchronous register. Here, the new register 134′ includes an asynchronous value input (“X”) and a control input for power that switches the register between the normal register value and the asynchronous value, depending upon whether the power is either on or off.
With conventional verification systems, all such components in a design would undergo some form of transformation to implement the formal verification process. The problem is that in large modern designs, there may be many millions or more of these components in the design. The transformation of all of these components consumes an inordinate amount of computing resources, and may create lengthy and very expensive delays for the design process.
Therefore, there is a need for an improved approach to implement transformations for verification of electronic circuit designs.